H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.601 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule Main

((encodeFloat :: Integer -> Int -> Float) :: Integer -> Int -> Float)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((encodeFloat :: Integer -> Int -> Float) :: Integer -> Int -> Float)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

power vw 0 = 1.0

power x vx@(y+1) = fromInt x * power x y

power x y = 1.0 / power x (`negate` y)

is transformed to

power vw xu = power4 vw xu

power x vx = power2 x vx

power x y = power0 x y

power0 x y = 1.0 / power x (`negate` y)

power1 True x vx = fromInt x * power x (vx - 1)

power1 wv ww wx = power0 ww wx

power2 x vx = power1 (vx >= 1) x vx

power2 wy wz = power0 wy wz

power3 True vw xu = 1.0

power3 xv xw xx = power2 xw xx

power4 vw xu = power3 (xu == 0) vw xu

power4 xy xz = power2 xy xz

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

mainModule Main

((encodeFloat :: Integer -> Int -> Float) :: Integer -> Int -> Float)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

fromInteger x * power 2 y

where

power vw xu = power4 vw xu

power x vx = power2 x vx

power x y = power0 x y

power0 x y = 1.0 / power x (`negate` y)

power1 True x vx = fromInt x * power x (vx - 1)

power1 wv ww wx = power0 ww wx

power2 x vx = power1 (vx >= 1) x vx

power2 wy wz = power0 wy wz

power3 True vw xu = 1.0

power3 xv xw xx = power2 xw xx

power4 vw xu = power3 (xu == 0) vw xu

power4 xy xz = power2 xy xz

are unpacked to the following functions on top level

primFloatEncodePower1 True x vx = fromInt x * primFloatEncodePower x (vx - 1)

primFloatEncodePower1 wv ww wx = primFloatEncodePower0 ww wx

primFloatEncodePower3 True vw xu = 1.0

primFloatEncodePower3 xv xw xx = primFloatEncodePower2 xw xx

primFloatEncodePower4 vw xu = primFloatEncodePower3 (xu == 0) vw xu

primFloatEncodePower4 xy xz = primFloatEncodePower2 xy xz

primFloatEncodePower0 x y = 1.0 / primFloatEncodePower x (`negate` y)

primFloatEncodePower vw xu = primFloatEncodePower4 vw xu

primFloatEncodePower x vx = primFloatEncodePower2 x vx

primFloatEncodePower x y = primFloatEncodePower0 x y

primFloatEncodePower2 x vx = primFloatEncodePower1 (vx >= 1) x vx

primFloatEncodePower2 wy wz = primFloatEncodePower0 wy wz

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

mainModule Main

((encodeFloat :: Integer -> Int -> Float) :: Integer -> Int -> Float)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

mainModule Main

(encodeFloat :: Integer -> Int -> Float)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="encodeFloat",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="encodeFloat yu3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="encodeFloat yu3 yu4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="primFloatEncode yu3 yu4",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="fromInteger yu3 * primFloatEncodePower (Pos (Succ (Succ Zero))) yu4",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="primMulFloat (fromInteger yu3) (primFloatEncodePower (Pos (Succ (Succ Zero))) yu4)",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="primMulFloat (primIntegerToFloat yu3) (primFloatEncodePower (Pos (Succ (Succ Zero))) yu4)",fontsize=16,color="burlywood",shape="box"];268[label="yu3/Integer yu30",fontsize=10,color="white",style="solid",shape="box"];8 -> 268[label="",style="solid", color="burlywood", weight=9];
268 -> 9[label="",style="solid", color="burlywood", weight=3];
9[label="primMulFloat (primIntegerToFloat (Integer yu30)) (primFloatEncodePower (Pos (Succ (Succ Zero))) yu4)",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10[label="primMulFloat (primIntToFloat yu30) (primFloatEncodePower (Pos (Succ (Succ Zero))) yu4)",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11 -> 87[label="",style="dashed", color="red", weight=0];
11[label="primMulFloat (Float yu30 (Pos (Succ Zero))) (primFloatEncodePower (Pos (Succ (Succ Zero))) yu4)",fontsize=16,color="magenta"];11 -> 88[label="",style="dashed", color="magenta", weight=3];
88[label="primFloatEncodePower (Pos (Succ (Succ Zero))) yu4",fontsize=16,color="black",shape="triangle"];88 -> 133[label="",style="solid", color="black", weight=3];
87[label="primMulFloat (Float yu30 (Pos (Succ Zero))) yu6",fontsize=16,color="burlywood",shape="triangle"];270[label="yu6/Float yu60 yu61",fontsize=10,color="white",style="solid",shape="box"];87 -> 270[label="",style="solid", color="burlywood", weight=9];
270 -> 134[label="",style="solid", color="burlywood", weight=3];
133[label="primFloatEncodePower4 (Pos (Succ (Succ Zero))) yu4",fontsize=16,color="black",shape="box"];133 -> 135[label="",style="solid", color="black", weight=3];
134[label="primMulFloat (Float yu30 (Pos (Succ Zero))) (Float yu60 yu61)",fontsize=16,color="black",shape="box"];134 -> 136[label="",style="solid", color="black", weight=3];
135[label="primFloatEncodePower3 (yu4 == Pos Zero) (Pos (Succ (Succ Zero))) yu4",fontsize=16,color="black",shape="box"];135 -> 137[label="",style="solid", color="black", weight=3];
136[label="Float (yu30 * yu60) (Pos (Succ Zero) * yu61)",fontsize=16,color="green",shape="box"];136 -> 138[label="",style="dashed", color="green", weight=3];
136 -> 139[label="",style="dashed", color="green", weight=3];
137[label="primFloatEncodePower3 (primEqInt yu4 (Pos Zero)) (Pos (Succ (Succ Zero))) yu4",fontsize=16,color="burlywood",shape="box"];271[label="yu4/Pos yu40",fontsize=10,color="white",style="solid",shape="box"];137 -> 271[label="",style="solid", color="burlywood", weight=9];
271 -> 140[label="",style="solid", color="burlywood", weight=3];
272[label="yu4/Neg yu40",fontsize=10,color="white",style="solid",shape="box"];137 -> 272[label="",style="solid", color="burlywood", weight=9];
272 -> 141[label="",style="solid", color="burlywood", weight=3];
138[label="yu30 * yu60",fontsize=16,color="black",shape="triangle"];138 -> 142[label="",style="solid", color="black", weight=3];
139 -> 138[label="",style="dashed", color="red", weight=0];
139[label="Pos (Succ Zero) * yu61",fontsize=16,color="magenta"];139 -> 143[label="",style="dashed", color="magenta", weight=3];
139 -> 144[label="",style="dashed", color="magenta", weight=3];
140[label="primFloatEncodePower3 (primEqInt (Pos yu40) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos yu40)",fontsize=16,color="burlywood",shape="box"];274[label="yu40/Succ yu400",fontsize=10,color="white",style="solid",shape="box"];140 -> 274[label="",style="solid", color="burlywood", weight=9];
274 -> 145[label="",style="solid", color="burlywood", weight=3];
275[label="yu40/Zero",fontsize=10,color="white",style="solid",shape="box"];140 -> 275[label="",style="solid", color="burlywood", weight=9];
275 -> 146[label="",style="solid", color="burlywood", weight=3];
141[label="primFloatEncodePower3 (primEqInt (Neg yu40) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg yu40)",fontsize=16,color="burlywood",shape="box"];276[label="yu40/Succ yu400",fontsize=10,color="white",style="solid",shape="box"];141 -> 276[label="",style="solid", color="burlywood", weight=9];
276 -> 147[label="",style="solid", color="burlywood", weight=3];
277[label="yu40/Zero",fontsize=10,color="white",style="solid",shape="box"];141 -> 277[label="",style="solid", color="burlywood", weight=9];
277 -> 148[label="",style="solid", color="burlywood", weight=3];
142[label="primMulInt yu30 yu60",fontsize=16,color="burlywood",shape="box"];278[label="yu30/Pos yu300",fontsize=10,color="white",style="solid",shape="box"];142 -> 278[label="",style="solid", color="burlywood", weight=9];
278 -> 149[label="",style="solid", color="burlywood", weight=3];
279[label="yu30/Neg yu300",fontsize=10,color="white",style="solid",shape="box"];142 -> 279[label="",style="solid", color="burlywood", weight=9];
279 -> 150[label="",style="solid", color="burlywood", weight=3];
143[label="yu61",fontsize=16,color="green",shape="box"];144[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];145[label="primFloatEncodePower3 (primEqInt (Pos (Succ yu400)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ yu400))",fontsize=16,color="black",shape="box"];145 -> 151[label="",style="solid", color="black", weight=3];
146[label="primFloatEncodePower3 (primEqInt (Pos Zero) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos Zero)",fontsize=16,color="black",shape="box"];146 -> 152[label="",style="solid", color="black", weight=3];
147[label="primFloatEncodePower3 (primEqInt (Neg (Succ yu400)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];147 -> 153[label="",style="solid", color="black", weight=3];
148[label="primFloatEncodePower3 (primEqInt (Neg Zero) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg Zero)",fontsize=16,color="black",shape="box"];148 -> 154[label="",style="solid", color="black", weight=3];
149[label="primMulInt (Pos yu300) yu60",fontsize=16,color="burlywood",shape="box"];280[label="yu60/Pos yu600",fontsize=10,color="white",style="solid",shape="box"];149 -> 280[label="",style="solid", color="burlywood", weight=9];
280 -> 155[label="",style="solid", color="burlywood", weight=3];
281[label="yu60/Neg yu600",fontsize=10,color="white",style="solid",shape="box"];149 -> 281[label="",style="solid", color="burlywood", weight=9];
281 -> 156[label="",style="solid", color="burlywood", weight=3];
150[label="primMulInt (Neg yu300) yu60",fontsize=16,color="burlywood",shape="box"];282[label="yu60/Pos yu600",fontsize=10,color="white",style="solid",shape="box"];150 -> 282[label="",style="solid", color="burlywood", weight=9];
282 -> 157[label="",style="solid", color="burlywood", weight=3];
283[label="yu60/Neg yu600",fontsize=10,color="white",style="solid",shape="box"];150 -> 283[label="",style="solid", color="burlywood", weight=9];
283 -> 158[label="",style="solid", color="burlywood", weight=3];
151[label="primFloatEncodePower3 False (Pos (Succ (Succ Zero))) (Pos (Succ yu400))",fontsize=16,color="black",shape="box"];151 -> 159[label="",style="solid", color="black", weight=3];
152[label="primFloatEncodePower3 True (Pos (Succ (Succ Zero))) (Pos Zero)",fontsize=16,color="black",shape="box"];152 -> 160[label="",style="solid", color="black", weight=3];
153[label="primFloatEncodePower3 False (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];153 -> 161[label="",style="solid", color="black", weight=3];
154[label="primFloatEncodePower3 True (Pos (Succ (Succ Zero))) (Neg Zero)",fontsize=16,color="black",shape="box"];154 -> 162[label="",style="solid", color="black", weight=3];
155[label="primMulInt (Pos yu300) (Pos yu600)",fontsize=16,color="black",shape="box"];155 -> 163[label="",style="solid", color="black", weight=3];
156[label="primMulInt (Pos yu300) (Neg yu600)",fontsize=16,color="black",shape="box"];156 -> 164[label="",style="solid", color="black", weight=3];
157[label="primMulInt (Neg yu300) (Pos yu600)",fontsize=16,color="black",shape="box"];157 -> 165[label="",style="solid", color="black", weight=3];
158[label="primMulInt (Neg yu300) (Neg yu600)",fontsize=16,color="black",shape="box"];158 -> 166[label="",style="solid", color="black", weight=3];
159[label="primFloatEncodePower2 (Pos (Succ (Succ Zero))) (Pos (Succ yu400))",fontsize=16,color="black",shape="box"];159 -> 167[label="",style="solid", color="black", weight=3];
160[label="fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="triangle"];160 -> 168[label="",style="solid", color="black", weight=3];
161[label="primFloatEncodePower2 (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];161 -> 169[label="",style="solid", color="black", weight=3];
162 -> 160[label="",style="dashed", color="red", weight=0];
162[label="fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="magenta"];163[label="Pos (primMulNat yu300 yu600)",fontsize=16,color="green",shape="box"];163 -> 170[label="",style="dashed", color="green", weight=3];
164[label="Neg (primMulNat yu300 yu600)",fontsize=16,color="green",shape="box"];164 -> 171[label="",style="dashed", color="green", weight=3];
165[label="Neg (primMulNat yu300 yu600)",fontsize=16,color="green",shape="box"];165 -> 172[label="",style="dashed", color="green", weight=3];
166[label="Pos (primMulNat yu300 yu600)",fontsize=16,color="green",shape="box"];166 -> 173[label="",style="dashed", color="green", weight=3];
167[label="primFloatEncodePower1 (Pos (Succ yu400) >= Pos (Succ Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ yu400))",fontsize=16,color="black",shape="box"];167 -> 174[label="",style="solid", color="black", weight=3];
168[label="doubleToFloat (Double (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];168 -> 175[label="",style="solid", color="black", weight=3];
169[label="primFloatEncodePower1 (Neg (Succ yu400) >= Pos (Succ Zero)) (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];169 -> 176[label="",style="solid", color="black", weight=3];
170[label="primMulNat yu300 yu600",fontsize=16,color="burlywood",shape="triangle"];285[label="yu300/Succ yu3000",fontsize=10,color="white",style="solid",shape="box"];170 -> 285[label="",style="solid", color="burlywood", weight=9];
285 -> 177[label="",style="solid", color="burlywood", weight=3];
286[label="yu300/Zero",fontsize=10,color="white",style="solid",shape="box"];170 -> 286[label="",style="solid", color="burlywood", weight=9];
286 -> 178[label="",style="solid", color="burlywood", weight=3];
171 -> 170[label="",style="dashed", color="red", weight=0];
171[label="primMulNat yu300 yu600",fontsize=16,color="magenta"];171 -> 179[label="",style="dashed", color="magenta", weight=3];
172 -> 170[label="",style="dashed", color="red", weight=0];
172[label="primMulNat yu300 yu600",fontsize=16,color="magenta"];172 -> 180[label="",style="dashed", color="magenta", weight=3];
173 -> 170[label="",style="dashed", color="red", weight=0];
173[label="primMulNat yu300 yu600",fontsize=16,color="magenta"];173 -> 181[label="",style="dashed", color="magenta", weight=3];
173 -> 182[label="",style="dashed", color="magenta", weight=3];
174[label="primFloatEncodePower1 (compare (Pos (Succ yu400)) (Pos (Succ Zero)) /= LT) (Pos (Succ (Succ Zero))) (Pos (Succ yu400))",fontsize=16,color="black",shape="box"];174 -> 183[label="",style="solid", color="black", weight=3];
175[label="Float (Pos (Succ Zero)) (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];176[label="primFloatEncodePower1 (compare (Neg (Succ yu400)) (Pos (Succ Zero)) /= LT) (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];176 -> 184[label="",style="solid", color="black", weight=3];
177[label="primMulNat (Succ yu3000) yu600",fontsize=16,color="burlywood",shape="box"];290[label="yu600/Succ yu6000",fontsize=10,color="white",style="solid",shape="box"];177 -> 290[label="",style="solid", color="burlywood", weight=9];
290 -> 185[label="",style="solid", color="burlywood", weight=3];
291[label="yu600/Zero",fontsize=10,color="white",style="solid",shape="box"];177 -> 291[label="",style="solid", color="burlywood", weight=9];
291 -> 186[label="",style="solid", color="burlywood", weight=3];
178[label="primMulNat Zero yu600",fontsize=16,color="burlywood",shape="box"];292[label="yu600/Succ yu6000",fontsize=10,color="white",style="solid",shape="box"];178 -> 292[label="",style="solid", color="burlywood", weight=9];
292 -> 187[label="",style="solid", color="burlywood", weight=3];
293[label="yu600/Zero",fontsize=10,color="white",style="solid",shape="box"];178 -> 293[label="",style="solid", color="burlywood", weight=9];
293 -> 188[label="",style="solid", color="burlywood", weight=3];
179[label="yu600",fontsize=16,color="green",shape="box"];180[label="yu300",fontsize=16,color="green",shape="box"];181[label="yu600",fontsize=16,color="green",shape="box"];182[label="yu300",fontsize=16,color="green",shape="box"];183[label="primFloatEncodePower1 (not (compare (Pos (Succ yu400)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yu400))",fontsize=16,color="black",shape="box"];183 -> 189[label="",style="solid", color="black", weight=3];
184[label="primFloatEncodePower1 (not (compare (Neg (Succ yu400)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];184 -> 190[label="",style="solid", color="black", weight=3];
185[label="primMulNat (Succ yu3000) (Succ yu6000)",fontsize=16,color="black",shape="box"];185 -> 191[label="",style="solid", color="black", weight=3];
186[label="primMulNat (Succ yu3000) Zero",fontsize=16,color="black",shape="box"];186 -> 192[label="",style="solid", color="black", weight=3];
187[label="primMulNat Zero (Succ yu6000)",fontsize=16,color="black",shape="box"];187 -> 193[label="",style="solid", color="black", weight=3];
188[label="primMulNat Zero Zero",fontsize=16,color="black",shape="box"];188 -> 194[label="",style="solid", color="black", weight=3];
189[label="primFloatEncodePower1 (not (primCmpInt (Pos (Succ yu400)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yu400))",fontsize=16,color="black",shape="box"];189 -> 195[label="",style="solid", color="black", weight=3];
190[label="primFloatEncodePower1 (not (primCmpInt (Neg (Succ yu400)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];190 -> 196[label="",style="solid", color="black", weight=3];
191 -> 197[label="",style="dashed", color="red", weight=0];
191[label="primPlusNat (primMulNat yu3000 (Succ yu6000)) (Succ yu6000)",fontsize=16,color="magenta"];191 -> 198[label="",style="dashed", color="magenta", weight=3];
192[label="Zero",fontsize=16,color="green",shape="box"];193[label="Zero",fontsize=16,color="green",shape="box"];194[label="Zero",fontsize=16,color="green",shape="box"];195[label="primFloatEncodePower1 (not (primCmpNat (Succ yu400) (Succ Zero) == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yu400))",fontsize=16,color="black",shape="box"];195 -> 199[label="",style="solid", color="black", weight=3];
196[label="primFloatEncodePower1 (not (LT == LT)) (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];196 -> 200[label="",style="solid", color="black", weight=3];
198 -> 170[label="",style="dashed", color="red", weight=0];
198[label="primMulNat yu3000 (Succ yu6000)",fontsize=16,color="magenta"];198 -> 201[label="",style="dashed", color="magenta", weight=3];
198 -> 202[label="",style="dashed", color="magenta", weight=3];
197[label="primPlusNat yu7 (Succ yu6000)",fontsize=16,color="burlywood",shape="triangle"];296[label="yu7/Succ yu70",fontsize=10,color="white",style="solid",shape="box"];197 -> 296[label="",style="solid", color="burlywood", weight=9];
296 -> 203[label="",style="solid", color="burlywood", weight=3];
297[label="yu7/Zero",fontsize=10,color="white",style="solid",shape="box"];197 -> 297[label="",style="solid", color="burlywood", weight=9];
297 -> 204[label="",style="solid", color="burlywood", weight=3];
199[label="primFloatEncodePower1 (not (primCmpNat yu400 Zero == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yu400))",fontsize=16,color="burlywood",shape="box"];298[label="yu400/Succ yu4000",fontsize=10,color="white",style="solid",shape="box"];199 -> 298[label="",style="solid", color="burlywood", weight=9];
298 -> 205[label="",style="solid", color="burlywood", weight=3];
299[label="yu400/Zero",fontsize=10,color="white",style="solid",shape="box"];199 -> 299[label="",style="solid", color="burlywood", weight=9];
299 -> 206[label="",style="solid", color="burlywood", weight=3];
200[label="primFloatEncodePower1 (not True) (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];200 -> 207[label="",style="solid", color="black", weight=3];
201[label="Succ yu6000",fontsize=16,color="green",shape="box"];202[label="yu3000",fontsize=16,color="green",shape="box"];203[label="primPlusNat (Succ yu70) (Succ yu6000)",fontsize=16,color="black",shape="box"];203 -> 208[label="",style="solid", color="black", weight=3];
204[label="primPlusNat Zero (Succ yu6000)",fontsize=16,color="black",shape="box"];204 -> 209[label="",style="solid", color="black", weight=3];
205[label="primFloatEncodePower1 (not (primCmpNat (Succ yu4000) Zero == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yu4000)))",fontsize=16,color="black",shape="box"];205 -> 210[label="",style="solid", color="black", weight=3];
206[label="primFloatEncodePower1 (not (primCmpNat Zero Zero == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];206 -> 211[label="",style="solid", color="black", weight=3];
207[label="primFloatEncodePower1 False (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];207 -> 212[label="",style="solid", color="black", weight=3];
208[label="Succ (Succ (primPlusNat yu70 yu6000))",fontsize=16,color="green",shape="box"];208 -> 213[label="",style="dashed", color="green", weight=3];
209[label="Succ yu6000",fontsize=16,color="green",shape="box"];210[label="primFloatEncodePower1 (not (GT == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yu4000)))",fontsize=16,color="black",shape="box"];210 -> 214[label="",style="solid", color="black", weight=3];
211[label="primFloatEncodePower1 (not (EQ == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];211 -> 215[label="",style="solid", color="black", weight=3];
212[label="primFloatEncodePower0 (Pos (Succ (Succ Zero))) (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];212 -> 216[label="",style="solid", color="black", weight=3];
213[label="primPlusNat yu70 yu6000",fontsize=16,color="burlywood",shape="triangle"];300[label="yu70/Succ yu700",fontsize=10,color="white",style="solid",shape="box"];213 -> 300[label="",style="solid", color="burlywood", weight=9];
300 -> 217[label="",style="solid", color="burlywood", weight=3];
301[label="yu70/Zero",fontsize=10,color="white",style="solid",shape="box"];213 -> 301[label="",style="solid", color="burlywood", weight=9];
301 -> 218[label="",style="solid", color="burlywood", weight=3];
214[label="primFloatEncodePower1 (not False) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yu4000)))",fontsize=16,color="black",shape="box"];214 -> 219[label="",style="solid", color="black", weight=3];
215[label="primFloatEncodePower1 (not False) (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];215 -> 220[label="",style="solid", color="black", weight=3];
216 -> 221[label="",style="dashed", color="red", weight=0];
216[label="fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero))) / primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yu400))",fontsize=16,color="magenta"];216 -> 222[label="",style="dashed", color="magenta", weight=3];
216 -> 223[label="",style="dashed", color="magenta", weight=3];
217[label="primPlusNat (Succ yu700) yu6000",fontsize=16,color="burlywood",shape="box"];303[label="yu6000/Succ yu60000",fontsize=10,color="white",style="solid",shape="box"];217 -> 303[label="",style="solid", color="burlywood", weight=9];
303 -> 224[label="",style="solid", color="burlywood", weight=3];
304[label="yu6000/Zero",fontsize=10,color="white",style="solid",shape="box"];217 -> 304[label="",style="solid", color="burlywood", weight=9];
304 -> 225[label="",style="solid", color="burlywood", weight=3];
218[label="primPlusNat Zero yu6000",fontsize=16,color="burlywood",shape="box"];305[label="yu6000/Succ yu60000",fontsize=10,color="white",style="solid",shape="box"];218 -> 305[label="",style="solid", color="burlywood", weight=9];
305 -> 226[label="",style="solid", color="burlywood", weight=3];
306[label="yu6000/Zero",fontsize=10,color="white",style="solid",shape="box"];218 -> 306[label="",style="solid", color="burlywood", weight=9];
306 -> 227[label="",style="solid", color="burlywood", weight=3];
219[label="primFloatEncodePower1 True (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yu4000)))",fontsize=16,color="black",shape="box"];219 -> 228[label="",style="solid", color="black", weight=3];
220[label="primFloatEncodePower1 True (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];220 -> 229[label="",style="solid", color="black", weight=3];
222 -> 160[label="",style="dashed", color="red", weight=0];
222[label="fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="magenta"];223 -> 88[label="",style="dashed", color="red", weight=0];
223[label="primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yu400))",fontsize=16,color="magenta"];223 -> 230[label="",style="dashed", color="magenta", weight=3];
221[label="yu9 / yu8",fontsize=16,color="black",shape="triangle"];221 -> 231[label="",style="solid", color="black", weight=3];
224[label="primPlusNat (Succ yu700) (Succ yu60000)",fontsize=16,color="black",shape="box"];224 -> 232[label="",style="solid", color="black", weight=3];
225[label="primPlusNat (Succ yu700) Zero",fontsize=16,color="black",shape="box"];225 -> 233[label="",style="solid", color="black", weight=3];
226[label="primPlusNat Zero (Succ yu60000)",fontsize=16,color="black",shape="box"];226 -> 234[label="",style="solid", color="black", weight=3];
227[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];227 -> 235[label="",style="solid", color="black", weight=3];
228 -> 236[label="",style="dashed", color="red", weight=0];
228[label="fromInt (Pos (Succ (Succ Zero))) * primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yu4000)) - Pos (Succ Zero))",fontsize=16,color="magenta"];228 -> 237[label="",style="dashed", color="magenta", weight=3];
229 -> 236[label="",style="dashed", color="red", weight=0];
229[label="fromInt (Pos (Succ (Succ Zero))) * primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="magenta"];229 -> 238[label="",style="dashed", color="magenta", weight=3];
230[label="`negate` Neg (Succ yu400)",fontsize=16,color="black",shape="box"];230 -> 239[label="",style="solid", color="black", weight=3];
231[label="primDivFloat yu9 yu8",fontsize=16,color="burlywood",shape="box"];311[label="yu9/Float yu90 yu91",fontsize=10,color="white",style="solid",shape="box"];231 -> 311[label="",style="solid", color="burlywood", weight=9];
311 -> 240[label="",style="solid", color="burlywood", weight=3];
232[label="Succ (Succ (primPlusNat yu700 yu60000))",fontsize=16,color="green",shape="box"];232 -> 241[label="",style="dashed", color="green", weight=3];
233[label="Succ yu700",fontsize=16,color="green",shape="box"];234[label="Succ yu60000",fontsize=16,color="green",shape="box"];235[label="Zero",fontsize=16,color="green",shape="box"];237 -> 88[label="",style="dashed", color="red", weight=0];
237[label="primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yu4000)) - Pos (Succ Zero))",fontsize=16,color="magenta"];237 -> 242[label="",style="dashed", color="magenta", weight=3];
236[label="fromInt (Pos (Succ (Succ Zero))) * yu10",fontsize=16,color="black",shape="triangle"];236 -> 243[label="",style="solid", color="black", weight=3];
238 -> 88[label="",style="dashed", color="red", weight=0];
238[label="primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="magenta"];238 -> 244[label="",style="dashed", color="magenta", weight=3];
239[label="primNegInt (Neg (Succ yu400))",fontsize=16,color="black",shape="box"];239 -> 245[label="",style="solid", color="black", weight=3];
240[label="primDivFloat (Float yu90 yu91) yu8",fontsize=16,color="burlywood",shape="box"];314[label="yu8/Float yu80 yu81",fontsize=10,color="white",style="solid",shape="box"];240 -> 314[label="",style="solid", color="burlywood", weight=9];
314 -> 246[label="",style="solid", color="burlywood", weight=3];
241 -> 213[label="",style="dashed", color="red", weight=0];
241[label="primPlusNat yu700 yu60000",fontsize=16,color="magenta"];241 -> 247[label="",style="dashed", color="magenta", weight=3];
241 -> 248[label="",style="dashed", color="magenta", weight=3];
242[label="Pos (Succ (Succ yu4000)) - Pos (Succ Zero)",fontsize=16,color="black",shape="box"];242 -> 249[label="",style="solid", color="black", weight=3];
243[label="primMulFloat (fromInt (Pos (Succ (Succ Zero)))) yu10",fontsize=16,color="black",shape="box"];243 -> 250[label="",style="solid", color="black", weight=3];
244[label="Pos (Succ Zero) - Pos (Succ Zero)",fontsize=16,color="black",shape="box"];244 -> 251[label="",style="solid", color="black", weight=3];
245[label="Pos (Succ yu400)",fontsize=16,color="green",shape="box"];246[label="primDivFloat (Float yu90 yu91) (Float yu80 yu81)",fontsize=16,color="black",shape="box"];246 -> 252[label="",style="solid", color="black", weight=3];
247[label="yu60000",fontsize=16,color="green",shape="box"];248[label="yu700",fontsize=16,color="green",shape="box"];249[label="primMinusInt (Pos (Succ (Succ yu4000))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];249 -> 253[label="",style="solid", color="black", weight=3];
250[label="primMulFloat (primIntToFloat (Pos (Succ (Succ Zero)))) yu10",fontsize=16,color="black",shape="box"];250 -> 254[label="",style="solid", color="black", weight=3];
251[label="primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];251 -> 255[label="",style="solid", color="black", weight=3];
252[label="Float (yu90 * yu81) (yu91 * yu80)",fontsize=16,color="green",shape="box"];252 -> 256[label="",style="dashed", color="green", weight=3];
252 -> 257[label="",style="dashed", color="green", weight=3];
253[label="primMinusNat (Succ (Succ yu4000)) (Succ Zero)",fontsize=16,color="black",shape="box"];253 -> 258[label="",style="solid", color="black", weight=3];
254 -> 87[label="",style="dashed", color="red", weight=0];
254[label="primMulFloat (Float (Pos (Succ (Succ Zero))) (Pos (Succ Zero))) yu10",fontsize=16,color="magenta"];254 -> 259[label="",style="dashed", color="magenta", weight=3];
254 -> 260[label="",style="dashed", color="magenta", weight=3];
255[label="primMinusNat (Succ Zero) (Succ Zero)",fontsize=16,color="black",shape="box"];255 -> 261[label="",style="solid", color="black", weight=3];
256 -> 138[label="",style="dashed", color="red", weight=0];
256[label="yu90 * yu81",fontsize=16,color="magenta"];256 -> 262[label="",style="dashed", color="magenta", weight=3];
256 -> 263[label="",style="dashed", color="magenta", weight=3];
257 -> 138[label="",style="dashed", color="red", weight=0];
257[label="yu91 * yu80",fontsize=16,color="magenta"];257 -> 264[label="",style="dashed", color="magenta", weight=3];
257 -> 265[label="",style="dashed", color="magenta", weight=3];
258[label="primMinusNat (Succ yu4000) Zero",fontsize=16,color="black",shape="box"];258 -> 266[label="",style="solid", color="black", weight=3];
259[label="yu10",fontsize=16,color="green",shape="box"];260[label="Pos (Succ (Succ Zero))",fontsize=16,color="green",shape="box"];261[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];261 -> 267[label="",style="solid", color="black", weight=3];
262[label="yu81",fontsize=16,color="green",shape="box"];263[label="yu90",fontsize=16,color="green",shape="box"];264[label="yu80",fontsize=16,color="green",shape="box"];265[label="yu91",fontsize=16,color="green",shape="box"];266[label="Pos (Succ yu4000)",fontsize=16,color="green",shape="box"];267[label="Pos Zero",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu700), Succ(yu60000)) → new_primPlusNat(yu700, yu60000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(yu700), Succ(yu60000)) → new_primPlusNat(yu700, yu60000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu3000), Succ(yu6000)) → new_primMulNat(yu3000, Succ(yu6000))

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(yu3000), Succ(yu6000)) → new_primMulNat(yu3000, Succ(yu6000))
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primFloatEncodePower(Pos(Succ(Succ(yu4000)))) → new_primFloatEncodePower(Pos(Succ(yu4000)))
new_primFloatEncodePower(Pos(Succ(Zero))) → new_primFloatEncodePower(Pos(Zero))
new_primFloatEncodePower(Neg(Succ(yu400))) → new_primFloatEncodePower(Pos(Succ(yu400)))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ RuleRemovalProof

Q DP problem:
The TRS P consists of the following rules:

new_primFloatEncodePower(Pos(Succ(Succ(yu4000)))) → new_primFloatEncodePower(Pos(Succ(yu4000)))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primFloatEncodePower(Pos(Succ(Succ(yu4000)))) → new_primFloatEncodePower(Pos(Succ(yu4000)))

Used ordering: POLO with Polynomial interpretation [25]:

POL(Pos(x₁)) = 2·x₁
POL(Succ(x₁)) = 1 + 2·x₁
POL(new_primFloatEncodePower(x₁)) = 2·x₁

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ RuleRemovalProof

                              ↳ QDP

                                ↳ PisEmptyProof

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

power	vw 0	= 1.0
power	x vx@(y+1)	= fromInt x * power x y
power	x y	= 1.0 / power x (`negate` y)

power	vw xu	= power4 vw xu
power	x vx	= power2 x vx
power	x y	= power0 x y

power1	True x vx	= fromInt x * power x (vx - 1)
power1	wv ww wx	= power0 ww wx

power4	vw xu	= power3 (xu == 0) vw xu
power4	xy xz	= power2 xy xz

primFloatEncodePower1	True x vx	= fromInt x * primFloatEncodePower x (vx - 1)
primFloatEncodePower1	wv ww wx	= primFloatEncodePower0 ww wx

primFloatEncodePower3	True vw xu	= 1.0
primFloatEncodePower3	xv xw xx	= primFloatEncodePower2 xw xx

primFloatEncodePower4	vw xu	= primFloatEncodePower3 (xu == 0) vw xu
primFloatEncodePower4	xy xz	= primFloatEncodePower2 xy xz

primFloatEncodePower	vw xu	= primFloatEncodePower4 vw xu
primFloatEncodePower	x vx	= primFloatEncodePower2 x vx
primFloatEncodePower	x y	= primFloatEncodePower0 x y

primFloatEncodePower2	x vx	= primFloatEncodePower1 (vx >= 1) x vx
primFloatEncodePower2	wy wz	= primFloatEncodePower0 wy wz